R:es_realizer{i:l}, P:(ES{i}{i'}).
R-Feasible{i:l}
R-Feasible(R)
 d-realizes{i:l}
 d-realizes([[R]]; es.P(es))
 (es:ES{i}. R-possible{i:l}(R; es)  P(es)) 

latex

Definitions	x. t(x), t  T, x(s), P  Q, , x:A. B(x), P & Q, x:A. B(x), A c B, Possible(R;es), D realizes es. P(es)
Lemmas	es realizer wf, R-Feasible wf, d-es wf, d-realizes wf, event system wf, R-possible wf, d-sub-self, R-Dsys wf